Left Termination of the query pattern
p2_in_1(a)
w.r.t. the given Prolog program could not be shown:
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
Clauses:
p1(f(X)) :- p1(X).
p2(f(X)) :- p2(X).
Queries:
p2(a).
We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
p2_in: (f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
p2_in_a(f(X)) → U2_a(X, p2_in_a(X))
U2_a(X, p2_out_a(X)) → p2_out_a(f(X))
The argument filtering Pi contains the following mapping:
p2_in_a(x1) = p2_in_a
U2_a(x1, x2) = U2_a(x2)
p2_out_a(x1) = p2_out_a(x1)
f(x1) = f(x1)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PrologToPiTRSProof
Pi-finite rewrite system:
The TRS R consists of the following rules:
p2_in_a(f(X)) → U2_a(X, p2_in_a(X))
U2_a(X, p2_out_a(X)) → p2_out_a(f(X))
The argument filtering Pi contains the following mapping:
p2_in_a(x1) = p2_in_a
U2_a(x1, x2) = U2_a(x2)
p2_out_a(x1) = p2_out_a(x1)
f(x1) = f(x1)
Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
P2_IN_A(f(X)) → U2_A(X, p2_in_a(X))
P2_IN_A(f(X)) → P2_IN_A(X)
The TRS R consists of the following rules:
p2_in_a(f(X)) → U2_a(X, p2_in_a(X))
U2_a(X, p2_out_a(X)) → p2_out_a(f(X))
The argument filtering Pi contains the following mapping:
p2_in_a(x1) = p2_in_a
U2_a(x1, x2) = U2_a(x2)
p2_out_a(x1) = p2_out_a(x1)
f(x1) = f(x1)
U2_A(x1, x2) = U2_A(x2)
P2_IN_A(x1) = P2_IN_A
We have to consider all (P,R,Pi)-chains
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PrologToPiTRSProof
Pi DP problem:
The TRS P consists of the following rules:
P2_IN_A(f(X)) → U2_A(X, p2_in_a(X))
P2_IN_A(f(X)) → P2_IN_A(X)
The TRS R consists of the following rules:
p2_in_a(f(X)) → U2_a(X, p2_in_a(X))
U2_a(X, p2_out_a(X)) → p2_out_a(f(X))
The argument filtering Pi contains the following mapping:
p2_in_a(x1) = p2_in_a
U2_a(x1, x2) = U2_a(x2)
p2_out_a(x1) = p2_out_a(x1)
f(x1) = f(x1)
U2_A(x1, x2) = U2_A(x2)
P2_IN_A(x1) = P2_IN_A
We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 1 SCC with 1 less node.
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
Pi DP problem:
The TRS P consists of the following rules:
P2_IN_A(f(X)) → P2_IN_A(X)
The TRS R consists of the following rules:
p2_in_a(f(X)) → U2_a(X, p2_in_a(X))
U2_a(X, p2_out_a(X)) → p2_out_a(f(X))
The argument filtering Pi contains the following mapping:
p2_in_a(x1) = p2_in_a
U2_a(x1, x2) = U2_a(x2)
p2_out_a(x1) = p2_out_a(x1)
f(x1) = f(x1)
P2_IN_A(x1) = P2_IN_A
We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PrologToPiTRSProof
Pi DP problem:
The TRS P consists of the following rules:
P2_IN_A(f(X)) → P2_IN_A(X)
R is empty.
The argument filtering Pi contains the following mapping:
f(x1) = f(x1)
P2_IN_A(x1) = P2_IN_A
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PrologToPiTRSProof
Q DP problem:
The TRS P consists of the following rules:
P2_IN_A → P2_IN_A
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.
The TRS P consists of the following rules:
P2_IN_A → P2_IN_A
The TRS R consists of the following rules:none
s = P2_IN_A evaluates to t =P2_IN_A
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [ ]
Rewriting sequence
The DP semiunifies directly so there is only one rewrite step from P2_IN_A to P2_IN_A.
We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
p2_in: (f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
p2_in_a(f(X)) → U2_a(X, p2_in_a(X))
U2_a(X, p2_out_a(X)) → p2_out_a(f(X))
The argument filtering Pi contains the following mapping:
p2_in_a(x1) = p2_in_a
U2_a(x1, x2) = U2_a(x2)
p2_out_a(x1) = p2_out_a(x1)
f(x1) = f(x1)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
Pi-finite rewrite system:
The TRS R consists of the following rules:
p2_in_a(f(X)) → U2_a(X, p2_in_a(X))
U2_a(X, p2_out_a(X)) → p2_out_a(f(X))
The argument filtering Pi contains the following mapping:
p2_in_a(x1) = p2_in_a
U2_a(x1, x2) = U2_a(x2)
p2_out_a(x1) = p2_out_a(x1)
f(x1) = f(x1)
Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
P2_IN_A(f(X)) → U2_A(X, p2_in_a(X))
P2_IN_A(f(X)) → P2_IN_A(X)
The TRS R consists of the following rules:
p2_in_a(f(X)) → U2_a(X, p2_in_a(X))
U2_a(X, p2_out_a(X)) → p2_out_a(f(X))
The argument filtering Pi contains the following mapping:
p2_in_a(x1) = p2_in_a
U2_a(x1, x2) = U2_a(x2)
p2_out_a(x1) = p2_out_a(x1)
f(x1) = f(x1)
U2_A(x1, x2) = U2_A(x2)
P2_IN_A(x1) = P2_IN_A
We have to consider all (P,R,Pi)-chains
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
Pi DP problem:
The TRS P consists of the following rules:
P2_IN_A(f(X)) → U2_A(X, p2_in_a(X))
P2_IN_A(f(X)) → P2_IN_A(X)
The TRS R consists of the following rules:
p2_in_a(f(X)) → U2_a(X, p2_in_a(X))
U2_a(X, p2_out_a(X)) → p2_out_a(f(X))
The argument filtering Pi contains the following mapping:
p2_in_a(x1) = p2_in_a
U2_a(x1, x2) = U2_a(x2)
p2_out_a(x1) = p2_out_a(x1)
f(x1) = f(x1)
U2_A(x1, x2) = U2_A(x2)
P2_IN_A(x1) = P2_IN_A
We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 1 SCC with 1 less node.
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
Pi DP problem:
The TRS P consists of the following rules:
P2_IN_A(f(X)) → P2_IN_A(X)
The TRS R consists of the following rules:
p2_in_a(f(X)) → U2_a(X, p2_in_a(X))
U2_a(X, p2_out_a(X)) → p2_out_a(f(X))
The argument filtering Pi contains the following mapping:
p2_in_a(x1) = p2_in_a
U2_a(x1, x2) = U2_a(x2)
p2_out_a(x1) = p2_out_a(x1)
f(x1) = f(x1)
P2_IN_A(x1) = P2_IN_A
We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
Pi DP problem:
The TRS P consists of the following rules:
P2_IN_A(f(X)) → P2_IN_A(X)
R is empty.
The argument filtering Pi contains the following mapping:
f(x1) = f(x1)
P2_IN_A(x1) = P2_IN_A
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
Q DP problem:
The TRS P consists of the following rules:
P2_IN_A → P2_IN_A
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.
The TRS P consists of the following rules:
P2_IN_A → P2_IN_A
The TRS R consists of the following rules:none
s = P2_IN_A evaluates to t =P2_IN_A
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [ ]
Rewriting sequence
The DP semiunifies directly so there is only one rewrite step from P2_IN_A to P2_IN_A.